(* $Id: automaticProver.ml 68 2007-10-16 09:59:43Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

open XCoreSyntax

let ergo (f, (q, _)) = 
    (* FIXME: Ergo is not capable of deducing False from inconsistent 
       hypothesis. *)
    if f.fvalue = FFalse then
      Ergo.inconsistent_assumptions q 
    else Ergo.prove q

let simplify (_, (_, q)) = 
  Simplify.prove q

let trivial_prover (f, _) =
  TrivialProver.prove f

let rec try_with_provers failed_filenames query = function
  | [] -> (false, failed_filenames)
  | prover :: others -> 
      let (ret, filename) = prover query in
	if not ret then 
	  try_with_provers (filename :: failed_filenames) query others 
	else 
	  (ret, [filename])
    
let prove f (env, ef) =
  try_with_provers
    []
    (f, (PFOLEnv.proof_obligation_to_query env ef))
    [
      trivial_prover;
      ergo;
      simplify;
    ]
